(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(x, y) → g1(x, x, y)
f(x, y) → g1(y, x, x)
f(x, y) → g2(x, y, y)
f(x, y) → g2(y, y, x)
g1(x, x, y) → h(x, y)
g1(y, x, x) → h(x, y)
g2(x, y, y) → h(x, y)
g2(y, y, x) → h(x, y)
h(x, x) → x
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, z1) → g1(z0, z0, z1)
f(z0, z1) → g1(z1, z0, z0)
f(z0, z1) → g2(z0, z1, z1)
f(z0, z1) → g2(z1, z1, z0)
g1(z0, z0, z1) → h(z0, z1)
g1(z0, z1, z1) → h(z1, z0)
g2(z0, z1, z1) → h(z0, z1)
g2(z0, z0, z1) → h(z1, z0)
h(z0, z0) → z0
Tuples:
F(z0, z1) → c(G1(z0, z0, z1))
F(z0, z1) → c1(G1(z1, z0, z0))
F(z0, z1) → c2(G2(z0, z1, z1))
F(z0, z1) → c3(G2(z1, z1, z0))
G1(z0, z0, z1) → c4(H(z0, z1))
G1(z0, z1, z1) → c5(H(z1, z0))
G2(z0, z1, z1) → c6(H(z0, z1))
G2(z0, z0, z1) → c7(H(z1, z0))
S tuples:
F(z0, z1) → c(G1(z0, z0, z1))
F(z0, z1) → c1(G1(z1, z0, z0))
F(z0, z1) → c2(G2(z0, z1, z1))
F(z0, z1) → c3(G2(z1, z1, z0))
G1(z0, z0, z1) → c4(H(z0, z1))
G1(z0, z1, z1) → c5(H(z1, z0))
G2(z0, z1, z1) → c6(H(z0, z1))
G2(z0, z0, z1) → c7(H(z1, z0))
K tuples:none
Defined Rule Symbols:
f, g1, g2, h
Defined Pair Symbols:
F, G1, G2
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 8 trailing nodes:
F(z0, z1) → c(G1(z0, z0, z1))
G1(z0, z1, z1) → c5(H(z1, z0))
G2(z0, z1, z1) → c6(H(z0, z1))
F(z0, z1) → c3(G2(z1, z1, z0))
F(z0, z1) → c2(G2(z0, z1, z1))
F(z0, z1) → c1(G1(z1, z0, z0))
G1(z0, z0, z1) → c4(H(z0, z1))
G2(z0, z0, z1) → c7(H(z1, z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, z1) → g1(z0, z0, z1)
f(z0, z1) → g1(z1, z0, z0)
f(z0, z1) → g2(z0, z1, z1)
f(z0, z1) → g2(z1, z1, z0)
g1(z0, z0, z1) → h(z0, z1)
g1(z0, z1, z1) → h(z1, z0)
g2(z0, z1, z1) → h(z0, z1)
g2(z0, z0, z1) → h(z1, z0)
h(z0, z0) → z0
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
f, g1, g2, h
Defined Pair Symbols:none
Compound Symbols:none
(5) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(6) BOUNDS(O(1), O(1))